ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A,B:ecl-trans-tuple{i:l}(ds; da),
f:(()()), g:().
ecl-trans-normal(A)
 ecl-trans-normal(B)
 (m:. ((f((n.ff),n.ff,m))))
 ecl-trans-normal(combine-ecl-tuples(A; B; f; g)) 

latex

Definitions	t  T, x:A. B(x), b, P  Q, False, A, A  B, , P  Q, P  Q, P  Q, prop{i:l}, True, T, , x. t(x), , no_repeats(T; l), sorted(L), finite-type(T), decidable(P), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-normal(x), combine-ecl-tuples(A; B; f; g), ecl-trans-tuple{i:l}(ds; da), Id, fpf(A; a.B(a)), Knd, ff
Lemmas	bfalse wf, ecl-trans-normal wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, decidable equal product, no repeats-merge, sorted-merge, nat plus wf, finite-type-product, not wf, assert wf, squash wf, true wf, bool wf, nat wf, eqff to assert, assert of bnot